Nuprl Lemma : weak-send-do-apply_wf 11,40
es:ES, T:Type, l:IdLnk, tg, a:Id, ds:x:Id fp Type, f:(State(ds)(T + Top)).
weak-send-do-apply(es;T;l;tg;a;ds;f)   
latex

Definitionst  T, Top, x:AB(x), x:A. B(x), S  T, left + right, State(ds), suptype(S; T), can-apply(f;x), x:A  B(x), b, ES, Type, IdLnk, Atom$n, Id, a:A fp B(a), P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , {i..j}, , x.A(x), Void, x:A.B(x), f(x)?z, x. t(x), IdDeq, , f(a), do-apply(f;x), #$n, discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), weak-send-do-apply(es;T;l;tg;a;ds;f), True, T, SqStable(P)
Lemmassq stable from decidable, decidable assert, discrete-weak-precond-send-p wf, do-apply wf, int seg wf, decl-state wf, fpf wf, Id wf, IdLnk wf, event system wf, subtype rel function, fpf-cap wf, id-deq wf, top wf, subtype rel set, assert wf, can-apply wf

origin